\documentclass{llncs}

\usepackage{epsfig,amsfonts,latexsym,upref}%,xypic}
\usepackage{graphicx,color,cite,times}
\usepackage{amsmath,amssymb,dsfont,eufrak,mathrsfs}

\usepackage{galois}

\newtheorem{defn}{Definition}
\newenvironment{deff}{\begin{defn} \itshape}{\end{defn}}
\newtheorem{teo}{Theorem}
\newenvironment{teoo}{\begin{teo} \itshape}{\end{teo}}
\newtheorem{es}{Example}
\newenvironment{ess}{\begin{es} \itshape}{\end{es}}
\newtheorem{prop}{Proposition}
\newenvironment{propp}{\begin{prop} \itshape}{\end{prop}}      
\newtheorem{lem}{Lemma}
\newenvironment{lemm}{\begin{lem} \itshape}{\end{lem}}
\newtheorem{cor}{Corollary} 
\newenvironment{corr}{\begin{cor} \itshape}{\end{cor}}


% MACRO

%OK
\def\ok#1{\mbox{\raisebox{0ex}[1ex][1ex]{$#1$}}}



\def \tuple#1{\langle #1 \rangle}

\def\tr{\triangleright}
\def\ra{\rightarrow}
\def\la{\leftarrow}
\def\La{\Leftarrow}
\def\lra{\leftrightarrow}
\def\Ra{\Rightarrow}
\def\Lra{\Leftrightarrow}

\def\bt{\mathbf{t}}
\def\bs{\mathbf{s}}
\def\cB{\mathcal{B}}
\def\cF{\mathcal{F}}
\def\uco{\mathit{uco}}
\def\gfp{\mathit{gfp}}
\def\lfp{\mathit{lfp}}
\def\back{\mathit{back}}
\def\succ{\mathit{succ}}
\def\next{\mathit{next}}
\def\ccs{\mathit{CCS}}
\def\rccs{\mathit{RCCS}}
\def\bccs{\mathbf{CCS}}
\def\brccs{\mathbf{RCCS}}

\newcommand{\sset}[2]{\left\{~#1  \left |
                    \begin{array}{l}#2\end{array} \right.     \right\}}

\def\grass#1{[\![#1]\!]}

\pagestyle{plain}

\begin{document}

\title{Modeling Reversibility as\\ Abstract Domain Completeness}

%\author{}
			
%\institute{}


\maketitle

%\begin{abstract} In this paper \dots
%\emph{Keywords:} %\end{abstract}

\section{Introduction}

\section{Background}

\subsection{Mathematical Notation}
\begin{itemize}
\item sets, order relation, poset, complete lattice, isomorphism
\item $\sqsubseteq$ order on functions, function composition
\item additive, co-additive, continuous, monotone functions
\item lfp and gfp
\end{itemize}

\subsection{Completeness in Abstract Interpretation}
We consider here the standard Galois-connection-based abstract interpretation theory introduced in ~\cite{CC77}. Abstract interpretation is based on the idea that the behaviour of a program at different levels of abstraction is an approximation of its (concrete) semantics~\cite{CC77,CC79}. The concrete program semantics is computed on the concrete domain $\tuple{C,\leq_C}$ while approximation is encoded by an abstract domain $\tuple{A,\leq_A}$. In abstract interpretation the concrete and abstract domains are complete lattices and abstraction is specified as a Galois connection (GC) $(C,\alpha,\gamma,A)$, i.e., an adjunction~\cite{CC77,CC79}, namely as an abstraction map $\alpha: C \ra A$ and a concretization map $\gamma: A \ra C$ such that: $\forall a \in A, c \in C: \alpha(c) \leq_A a \Lra c \leq_C \gamma(a)$. $\alpha$ (reps.\ $\gamma$) is the left- (right-) adjoint to $\gamma$ (reps.\ $\alpha$) and it is an additive (reps.\ co-additive) function. Given and additive function $f$ its right adjoint is $f^+ = \lambda x . \bigvee \{y ~|~ f(y) \leq x\}$, while given a co-additive function $f$ its left adjoint is $f^- = \lambda x . \bigwedge \{y ~|~ x \leq f(y)\}$. We have a Galois insertion (GI) when for every abstract element $a$ in $A$ we have that $\alpha(\gamma(a)) = a$.

Given a poset $C$, an \emph{upper closure operator} $\rho: C \ra C$ is a function that is monotone, idempotent and extensive: $\forall c \in C: c \leq \rho(c)$. We denote with $\uco(C)$ the set of upper closure operators over $C$. Every closure operator $\rho \in \uco(C)$ is uniquely determined by the set of its fix-points $\rho(C)$. Given a subset $X$ of $C$, we have that $X$ is the set of fix-points of an upper closure operator $\rho \in \uco(C)$ if and only if $X$ is a Moore family of $C$, i.e.\, $X  = \mathcal{M}(X) = \{ \wedge S ~|~ S \subseteq X\}$, $\wedge \emptyset = \top \in \mathcal{M}(X)$, if and only if $X$ is isomorphic to an abstract domain $A$ in a GI $(C,\alpha,\gamma,A)$, i.e.\, $A  \approx \rho(C)$ with $\rho = \gamma \circ \alpha$.
%
$\uco(C)$ is isomorphic to the so called \emph{lattice of abstract interpretations} of $C$~\cite{CC79}. If $C$ is a complete lattice then $\tuple{\uco(C), \sqsubseteq, \sqcup, \sqcap, \lambda x. \top, \lambda x.x}$ is also a complete lattice, where for every $\rho, \eta \in \uco(C)$, $\{\rho_i\}_{i \in I} \subseteq \uco(C)$ and  $x \in C$: $\rho \sqsubseteq \eta$ if and only if $\eta(C) \subseteq \rho(C)$; $(\sqcap_{i \in I} \rho_i)(x) = \wedge_{i \in I} \rho_i(x)$; and $(\sqcup_{i \in I} \rho_i)(x) = x \; \Lra \;  \forall i \in I: \rho_i(x) = x$. 

Given a GI $(C,\alpha,\gamma,A)$ we say that a function $f^\sharp: A \ra A$ is a \emph{sound} approximation of function $f:C \ra C$ if $\alpha \circ f \sqsubseteq f^\sharp \circ \alpha$, or equivalently, by adjunction, if $f \circ \gamma \sqsubseteq \gamma \circ f^\sharp$. The \emph{best correct approximation} of $f$ is $f^{\mathit{bca}} = \alpha \circ f \circ \gamma$ (or equivalently $\gamma \circ \alpha \circ f \circ \gamma \circ \alpha$). Thus, $f^\sharp$ is sound if and only if $f^\mathit{bca} \sqsubseteq f^\sharp$. These equivalent notions of soundness lead to two distinct notions of completeness when equality is required. We speak of \emph{backward completeness} ($\mathcal{B}$-completeness) when $\alpha \circ f  = f^\sharp \circ \alpha$ and of \emph{forward completeness} ($\mathcal{F}$-completeness)  when $f \comp \gamma = \gamma \comp f^\sharp$. It has been proved that both $\mathcal{B}$-completeness and $\mathcal{F}$-completeness are domain properties, namely that there exists a backward of forward approximation of a function $f$ on an abstract domain $\rho \in \uco(C)$ if and only if the best correct approximation $\rho \circ f \circ \rho$ is respectively backward or forward complete, i.e.\, $\rho \circ f  = \rho \circ f \circ \rho$ or $f \circ \rho = \rho \circ f \circ \rho$~\cite{GQ01,GRSjacm}. This result has lead to the definition of proper domain transformations that minimally modify an abstract domain in order to make it backward or forward complete for a given function~\cite{GQ01,GRSjacm}. Let $f: C \ra C$ be a continuous function and let us consider abstraction $\rho \in \uco(C)$. We say that $\rho$ is $\mathcal{B}$($\mathcal{F}$)-complete for $f$ if $\rho \circ f = \rho \circ f \circ \rho$ ($f \circ \rho = \rho \circ f \circ \rho$). A \emph{domain refinement} is a monotone function $\tau:\uco(C) \ra \uco(C)$ such that $X \subseteq \tau(X)$. In~\cite{GQ01,GRSjacm} the authors provide a constructive characterization of the most abstract refinement that makes a domain backward or forward complete for a given function.  Let us consider the following operators on closures:
\begin{center}
\begin{tabular}{ll}
$R^\mathcal{F}_f =$ & $\lambda X. \mathcal{M}(f(X))$\\
$R^\mathcal{B}_f =$ & $\lambda X. \mathcal{M}(\bigcup_{y \in X} \mbox{max}(f^{-1}(\downarrow y)))$\\
\end{tabular}
\end{center}
Let $l \in \{\mathcal{F},\mathcal{B}\}$, we have that the most abstract domain that refines $\rho$ and that is $l$-complete for $f$ is:
\[
\mathcal{R}^l_f(\rho) = \gfp (\lambda X. \rho \sqcap R^l_f(X))
\]
%$$$$$$ 


\section{Languages Reversibility}

\subsection{RCCS and CCS}

In~\cite{rccs} the authors present a reversible version of CCS called RCCS. In particular, given a process they allow it to backtrack to any \emph{casually equivalent} past. 

Let us consider the alphabet $\Sigma = \Sigma_\circ \cup \Sigma_\bullet \cup \{\tau, \tau_\bullet\}$ where $\Sigma_\circ$ contains the forward actions and it is ranged over by $\alpha$, and $\Sigma_\bullet$ contains the backward actions and it is ranged over by $\alpha_\bullet$. \\

\begin{tabular}{ll}
CCS\\
$\alpha ::=$ & $a \;|\; \bar{a} \;|\; \tau \;|\; \dots$\\
$P ::=$ & $\mathbf{0} \;|\; \Sigma \alpha_i . P_i \;|\; (P | P) \;|\; (a)P$\\
\end{tabular}\\

\begin{tabular}{ll}
RCCS\\
$m ::=$ & $\tuple{}  \;|\; \tuple{1} \cdot m \;|\; \tuple{2} \cdot m \;|\; \tuple{\ast,\alpha,P} \cdot m \;|\; \tuple{m',\alpha,P} \cdot m$\\
$R ::=$ & $m \tr P \;|\;  (R | R) \;|\; (a)R$\\
\end{tabular}\\

In RCCS a transition $\bt$ is given by a triplet $R \stackrel{\mu:\xi}{\longrightarrow}_\rccs S$ with $R$ and $S$ monitored processes, $\mu$ identifier and $\xi \in \Sigma$ action. $R$ is the source, $S$ is the target of $\bt$. Two transitions are co-initial if they have the same source, co-final if they have the same target, composable if the source of the second is the target of the first. A transition is forward or backward accordingly to the actin labeling it. A trace is a sequence of pairwise composable transitions.  We say that a trace is forward if it contains only forward transitions. The empty trace is devoted as $\varepsilon_R$. 

Two co-initial transitions $R \stackrel{\mu_1:\xi_1}{\longrightarrow}_\rccs S_1$ and $R\stackrel{\mu_2:\xi_2}{\longrightarrow}_\rccs S_2$ are \emph{concurrent} if $\mu_1 \cap \mu_2 = \emptyset$.

\begin{lemma}[Square]
Let $\bt_1 = R \stackrel{\mu_1:\xi_1}{\longrightarrow}_\rccs S_1$ and $\bt_2 = R\stackrel{\mu_2:\xi_2}{\longrightarrow}_\rccs S_2$ be concurrent transitions, there exists two co-final transitions $\bt_2 / \bt_1 = S_1 \stackrel{\mu_2:\xi_2}{\longrightarrow}_\rccs T$ and $\bt_1 / \bt_2 = S_2 \stackrel{\mu_1:\xi_1}{\longrightarrow}_\rccs T$.
\end{lemma}

\begin{definition}[Causal Equivalence]
The causal equivalence relation $\sim$, is the least equivalence relation between traces closed under composition and such that:
\begin{itemize}
\item $\bt_1 ; \bt_2 / \bt_1 \sim \bt_2 ; \bt_1 / \bt_2$;
\item $\bt ; \bt_\bullet \sim \varepsilon_R$;
\item $\bt_\bullet ; \bt \sim \varepsilon_R$.
\end{itemize}
\end{definition}
%
Thus, for example $\bt_1 \bt_2 \bt_{2,\bullet} \bt_3 \sim \bt_1 \bt_3$. Moreover, $\bt \sim \bs$ and $\bt' \sim \bs'$ then $\bt \bt' \sim \bs \bs'$.

In CCS a transition is a triplet $P \stackrel{\alpha}{\longrightarrow}_\ccs Q$, where $\alpha$ is always a forward action.


In the following we will abstract traces and consider only the sequences of actions that label their transitions. Namely, given a RCCS trace $\bt = R_1 \stackrel{\mu_1:\xi_1}{\longrightarrow}_\rccs R_2  \stackrel{\mu_2:\xi_2}{\longrightarrow}_\rccs R_3 \dots R_n \stackrel{\mu_n:\xi_n}{\longrightarrow}_\rccs R_{n+1}$ we consider $\pi(\bt) = \xi_1 \xi_2 \dots \xi_n$. The same for the traces in CCS $\pi(P_1 \stackrel{\alpha_1}{\longrightarrow}_\ccs P_2 \stackrel{\alpha_2}{\longrightarrow}_\ccs P_3 \dots P_n \stackrel{\alpha_n}{\longrightarrow}_\ccs P_{n+1}) = \alpha_1 \alpha_2 \dots \alpha_n$. 

In this context we introduce the \emph{forward projection} which is a function $F: \wp(\Sigma^\ast) \ra \wp(\Sigma_\circ)^\ast$ that given a set of traces in $\wp(\Sigma^\ast)$ considers only their forward behavior:
$$
\begin{array}{l}
F(X) = \sset{F(t)}{t \in X}\\
F(t) = s \in \Sigma_\circ^\ast \mbox{ such that } s \sim t\\
\end{array}
$$
%
based on the forward projection we can compute the set of all possible traces that can be obtained allowing reversibility from a forward trace, given a forward trace $s \in \Sigma_\circ^\ast$ we define:
$$
B(s) = \sset{t \in (\Sigma_\circ \cup \Sigma_\bullet)^\ast}{F(t) = s}
$$
The extension to set of forward traces is straightforward $B: \wp(\Sigma_\circ^\ast) \ra \wp(\Sigma^\ast)$ is defined as $B(X) = \{B(s) ~|~ s \in X\}$.


Given a RCCS process $R$ we denote with $\grass{R} \in \wp(\Sigma^\ast)$ the set of its traces, and given a CCS process $P$ we denote with $\grass{P} \in \wp(\Sigma_\circ^\ast)$ the set of its traces. We then consider the following sets:
$$
\begin{array}{ll}
\bccs = & \sset{X \in \wp(\Sigma_\circ^\ast)}{X = \grass{P}, P \in \ccs}\\
\brccs = & \sset{X \in \wp(\Sigma^\ast)}{X = \grass{R}, R \in \rccs}\\
\end{array}
$$
Let us consider the domains that we can obtain by considering the above sets up to causal equivalence: $\bccs_{/\sim}$ and $\brccs_{/\sim}$. Thus, every element is $\brccs_{/\sim}$ identifies all those RCCS processes that generate sets of traces that are causally equivalent (the same for $\bccs_{/\sim}$). In the following we refer to an element $X$ in $\brccs_{/\sim}$ also as $\grass{R}$, or simply as $R$, if $\grass{R} \sim X$ (the same for $\bccs_{/\sim}$). Observe that every element $\grass{R} \in \brccs_{/\sim}$ is such that $\grass{R} = \grass{R}_\circ \cup B(\grass{R}_\circ)$ where $\grass{R}_\circ = \grass{R} \cap \Sigma_\circ^\ast$.


\subsection{RCCS and CCS form a GI}


Let us consider the domain $\tuple{\mathbf{CCS}_{/\sim},\dot{\sqsubseteq}}$ where $P \,\dot{\sqsubseteq} \, Q$ iff $\grass{Q} \, \subseteq \,\grass{P}$, and the domain  $\tuple{\mathbf{RCCS}_{/\sim},\dot{\sqsubseteq}}$ with the same ordering. This means that a RCCS or CCS process is more concrete than another one if it allows more behaviors. 

{\bf to check}: $\tuple{\mathbf{CCS},\dot{\sqsubseteq}}$ and $\tuple{\mathbf{RCCS},\dot{\sqsubseteq}}$ are (complete) lattices: namely we have to prove that $\forall X,Y \in \mathbf{CCS}$ we have that $X \dot{\sqcup} Y, X \dot{\sqcap} Y \in \mathbf{CCS}$. It would be nice if $X \dot{\sqcup} Y = X \cap Y$ and  $X \dot{\sqcap} Y = X \cup Y$ since we would have the same lug e glb of the concrete domain considered in Section~\ref{sec:complete}.

We can define the following Galois connection:
\[
\tuple{\mathbf{RCCS},\dot{\sqsubseteq}} \galois{\alpha}{\gamma} \tuple{\mathbf{CCS},\dot{\sqsubseteq}}
\]
where the abstraction function $\alpha: \mathbf{RCCS} \ra \mathbf{CCS}$ is defined as follows:
\begin{itemize}
\item $\alpha(m \tr P) = P$
\item $\alpha(R | R) = \alpha(R) | \alpha(R)$
\item $\alpha((a)R) = (a)\alpha(R)$
\end{itemize}
Observe that the above abstraction function is exactly the forgetful map defined in~\cite{rccs}. 
%
\begin{lemma}
$\grass{\alpha(R)} = \grass{R}_\circ = \grass{R} \cap \Sigma^\ast_\circ$.
\end{lemma}
{\sc proof:} {\bf to be done}.\\

\noindent
The concretization function $\gamma: \mathbf{CCS} \ra \mathbf{RCCS}$ is defined as follows:
\begin{itemize}
\item $\gamma(P) = \tuple{} \tr P$
\end{itemize}
It is clear that $\tuple{} \tr P \, \dot{\sqsubseteq} \, P$ since in $\grass{\tuple{} \tr P}$ we have also backward actions. In fact: $\grass{\tuple{} \tr P} = \grass{P} \cup B(\grass{P})$.

\begin{lemma}
$(\rccs_{/\sim},\alpha,\gamma,\ccs_{/\sim})$ is a GI.
\end{lemma}
{\sc proof:} {\bf to be checked and completed}
\begin{itemize}
\item$\alpha$ is monotone: $R_1 \, \dot{\sqsubseteq} \, R_2$ means that $\grass{R_2} \subseteq \grass{R_2}$ and therefore $\grass{R_2}^F \subseteq \grass{R_2}^F$ which means that $\grass{\alpha(R_2)} \subseteq \grass{\alpha(R_1)}$ and therefore $\alpha(R_1) \,\dot{\sqsubseteq} \, \alpha(R_2)$.
%
\item $\gamma$ is monotone: $P_1 \, \dot{\sqsubseteq} \, P_2$ means that $\grass{P_2} \subseteq \grass{P_2}$. We show by induction on the length of the string that this implies that $\grass{\tuple{} \tr P_2} \subseteq \grass{\tuple{} \tr P_1}$. For every string $\sigma$ of length 1 we have that $\sigma$ is forward and therefore $\sigma \in \grass{\tuple{} \tr P_2} \Ra \sigma \in \grass{\tuple{} \tr P_1}$. Let us assume that this implication holds for the traces of length $n$ and let us prove that it holds also for the traces of length $n+1$. {\bf to be completed}
%
\item $\gamma \circ \alpha$ is extensive, namely we want to prove that $R \, \dot{\sqsubseteq} \,\gamma(\alpha(R))$: 
\begin{itemize}
\item $R = m \tr P$, in this case we have $\gamma(\alpha(m \tr P)) = \tuple{} \tr P$ and $\grass{\tuple{} \tr P} \subseteq \grass{m \tr P}$ and therefore $m \tr P \,  \dot{\sqsubseteq} \, \tuple{} \tr P$
%
\item $R = R_1 | R_2$, thus we have:
\begin{eqnarray*}
\gamma(\alpha(R_1|R_2)) & = & \gamma(\alpha(R_1) | \alpha(R_2))\\
& = & \gamma(\alpha(m_1 \tr P_1)  \alpha(m_2 \tr P_2))\\
& = & \gamma(P_1 | P_2)\\
& = & \tuple{} \tr P_1 | P_2\\
& = & \tuple{} \tr P_1 | \tuple \tr P_2\\
\end{eqnarray*}
and since $\grass{\tuple{} \tr P_1 | \tuple \tr P_2} \subseteq \grass{m_1 \tr P_1 | m_2 \tr P_2}$, we have that $R_1 | R_2 \, \dot{\sqsubseteq} \, \gamma(\alpha(R_1 | R_2))$.
%
\item $R = (a)R$, thus we have:
\begin{eqnarray*}
\gamma(\alpha((a)R)) & = & \gamma(\alpha((a) m \tr P))\\
& = & \gamma(\alpha(m \tr (a)P))\\
& = & \gamma((a)P)\\
& = & \tuple{} \tr (a) P\\
& = & (a) \tuple{} \tr P
\end{eqnarray*}
and since $\grass{\tuple{} \tr (a) P} \subseteq \grass{m \tr (a) P}$, we have that $(a) R \,\dot{\sqsubseteq} \, \gamma(\alpha((a) R))$.
\end{itemize}
\item $\alpha \circ \gamma$ is the identity: $\alpha(\gamma(P)) = P$
\end{itemize}
%
\begin{flushright}
$\Box$
\end{flushright}


{\bf to check} $\alpha$ is additive, namely it holds that $\alpha(R_1 \dot{\sqcup} R_2) = \alpha(R_1) \dot{\sqcup}  \alpha(R_2)$. Observe that $\alpha(R_1 \dot{\sqcup} R_2) = P$ such that $\grass{P} = \grass{R_1}_\circ \cap \grass{R_2}_\circ$, namely it is the program that contains the forward trace shared by $R_1$ and $R_2$. On the other hand $\alpha(R_1) \dot{\sqcup} \alpha(R_2) = \alpha(R_1) \cap \alpha(R_2)$ and it corresponds to the same set of traces.

{\bf to check} $\longrightarrow_\ccs$ is the BCA of $\longrightarrow_\rccs$ on the abstract domain $\bccs$??


\subsubsection*{Relation between CCS and RCCS}

In~\cite{rccs,t-rccs} the authors formalize the relation between the transitions in CCS and the ones in RCCS by proving the following implications:
\begin{enumerate}
\item If $P \ra_{\mathit{CCS}}^\ast Q$ and $\gamma(R) = P$, then $R \ra^\ast_\mathit{RCCS} S$ for some $S$ such that  $Q = \gamma(S)$;
\item $P \ra^\ast_\mathit{CCS} \gamma(R) \; \Lra \; \alpha(P) \ra^\ast_\mathit{RCCS} R$;
\item If $\tuple{} \tr P \ra_\mathit{RCCS}^\ast R$, then $P \ra^\ast_\mathit{CCS} \gamma(R)$ (this is in \cite{t-rccs} instead of point (2))
\end{enumerate}

{\bf to check} the above implications follow form the fact that $\longrightarrow_\ccs$ is the BCA of $\longrightarrow_\rccs$??

\subsubsection*{Irreversible actions}

Let $I$ be the set of irreversible actions, if $I$ contains every possible action then it means that all actions are irreversible and we have CCS, when $I = \emptyset$ then none of the  actions is irreversible and therefore we have RCCS. Let $\tuple{\mathbf{RCCS}_I,\dot{\sqsubseteq}}$ denote the domain of RCCS processes with $I$ the set of their irreversible actions.
We can define the following Galois connection:
\[
\mathbf{RCCS} \galois{\alpha_I}{\gamma_I} \mathbf{RCCS}_I
\]
where the abstraction function $\alpha_I: \mathbf{RCCS} \ra \mathbf{RCCS}_I$ is defined as follows:
\begin{itemize}
\item $\alpha_I(m \tr P) =  h(m) \tr P$
\item $\alpha_I(R | R) = \alpha_I(R) | \alpha_I(R)$
\item $\alpha_I((a)R) = (a)\alpha_I(R)$ if $a \not\in I$ and $\alpha_I((a)R) = (\bar{a})\alpha_I(R)$ if $a \in I$
\end{itemize}
where function $h$ transforms memories in order to block reversibility:
\begin{itemize}
\item $h(\tuple{}) = \tuple{}$
\item $h(\tuple{1} \cdot m) = \tuple{1} \cdot \rho(m)$
\item $h(\tuple{2} \cdot m) = \tuple{2} \cdot \rho(m)$
\item 
$$
\rho(\tuple{\ast,\alpha,P} \cdot m) =
\left\{
\begin{array}{ll}
\tuple{} & \mbox{ if } \alpha \in I\\
\tuple{\ast,\alpha,P} \cdot h(m) \mbox{ otherwise}
\end{array}
\right.
$$
\item 
$$
\rho(\tuple{m',\alpha,P} \cdot m) =
\left\{
\begin{array}{ll}
\tuple{} & \mbox{ if } \alpha \in I\\
\tuple{m',\alpha,P} \cdot h(m) \mbox{ otherwise}
\end{array}
\right.
$$
\end{itemize}
%
{\bf to do} prove that $\alpha_I$ is additive and derive the corresponding $\gamma_I$.


%---------------------------------------


\subsection{RCCS is a completeness refinement of CCS}\label{sec:complete}

We consider the alphabet $\Sigma = \Sigma_\circ \cup \Sigma_\bullet \cup \{\tau, \tau_\bullet\}$ and  the complete lattice given by $\tuple{\wp(\Sigma^\ast),\dot{\sqsubseteq},\dot{\sqcup},\dot{\sqcap},\emptyset,\Sigma^\ast}$, where given a pair of elements $X,Y \in \wp(\Sigma^\ast)$ we have that $X \, \dot{\sqsubseteq} \, Y$ if $Y \subseteq X$, $\emptyset$ is the top element and $\Sigma^\ast$ is the bottom element. Thus, an element $X$ is more precise than an element $Y$ if it allows more behaviors.
 
We then consider the complete lattice of abstract interpretations of $\wp(\Sigma^\ast)$, namely the domain of closure operators over $\wp(\Sigma^\ast)$, that is $\tuple{\uco(\wp(\Sigma^\ast)),\sqsubseteq}$. Given two closures $\rho_1$ and $\rho_2$ in $\uco(\wp(\Sigma^\ast))$ we have that:
\begin{itemize}
\item $\rho_1 \sqsubseteq \rho_2$ iff $\forall X \in \wp(\Sigma^\ast): \; \rho_1(X) \, \dot{\sqsubseteq} \, \rho_2(X)$ iff $\forall X \in \wp(\Sigma^\ast): \; \rho_2(X) \subseteq \rho_1(X)$ iff $\rho_2(\wp(\Sigma^\ast)) \subseteq \rho_1(\wp(\Sigma^\ast))$;
%
\item the glb between two closures is defined as follows:
\begin{eqnarray*}
\rho_1 \sqcap \rho_2 & = & \sqcup \sset{\rho}{\rho \sqsubseteq \rho_1, \rho \sqsubseteq \rho_2}\\
& = & \sqcup \sset{\rho}{\forall X \in \wp(\Sigma^\ast): \rho_1(X) \subseteq \rho(X), \rho_2(X) \subseteq \rho(X)}\\
& = & \sqcup \sset{\rho}{\forall X \in \wp(\Sigma^\ast): \rho_1(X) \cup \rho_2(X) \subseteq \rho(X)}\\
& = & \lambda X. \rho_1(X) \cup \rho_2(X)
\end{eqnarray*}
%
\item the lug between two closures is defined as follows:
\begin{eqnarray*}
\rho_1 \sqcup \rho_2 & = & \sqcap \sset{\rho}{\rho_1 \sqsubseteq \rho, \rho_2 \sqsubseteq \rho}\\
& = & \sqcap \sset{\rho}{\forall X \in \wp(\Sigma^\ast): \rho(X) \subseteq \rho_1(X), \rho(X) \subseteq \rho_2(X)}\\
& = & \sqcup \sset{\rho}{\forall X \in \wp(\Sigma^\ast): \rho(X) \subseteq \rho_1(X) \cap \rho_2(X)}\\
& = & \lambda X. \rho_1(X) \cap \rho_2(X)
\end{eqnarray*}
\end{itemize}
%
{\bf +++} Since $CCS$ and $RCCS$ are complete lattices (or Moore families) there exists a closure operator associated to each of them. 
\begin{itemize}
\item $\rho_\ccs:\wp(\Sigma^\ast) \ra \wp(\Sigma^\ast)$ is defined as follows:
$$
\rho_\ccs = \lambda X.
\left\{
\begin{array}{ll}
\top = \emptyset & \mbox{ if } X \not\subseteq \Sigma^\ast_\circ\\
\cup \sset{Y \in \wp(\Sigma^\ast)}{Y \subseteq X, Y = \grass{P}, P \in \ccs} & \mbox{ otherwise}\\
\end{array}
\right.
$$
observe that given $X \in \wp(\Sigma^\ast)$ we have that $\rho_\ccs(X) \subseteq X$ and therefore $X \, \dot{\sqsubseteq} \, \rho_\ccs(X)$. Thus, function $\rho_\ccs$ is extensive,  monotone and idempotent.
\item
$\rho_\rccs:\wp(\Sigma^\ast) \ra \wp(\Sigma^\ast)$ is defined as follows:
$$
\rho_\rccs = \lambda X.
\cup \sset{Y \in \wp(\Sigma^\ast)}{Y \subseteq X, Y = \grass{R}, R \in \rccs}
$$
observe that given $X \in \wp(\Sigma^\ast)$ we have that $\rho_\rccs(X) \subseteq X$ and therefore $X \, \dot{\sqsubseteq} \, \rho_\rccs(X)$. Thus, function $\rho_\ccs$ is extensive,  monotone and idempotent.
\end{itemize}
%
Thus, $\rho_\ccs,\rho_\rccs \in \uco(\wp(\Sigma^\ast))$ and 
$$
\rho_\rccs \sqsubseteq \rho_\ccs
$$
since $\forall X \in \wp(\Sigma^\ast)$ we have that $\rho_\rccs(X) \, \dot{\sqsubseteq} \, \rho_\ccs(X)$:
\begin{itemize}
\item if $X$ contains a backward action then $\rho_\ccs(X) = \top$ and therefore $\rho_\rccs(X) \, \dot{\sqsubseteq} \, \rho_\ccs(X)$;
\item otherwise $\rho_\rccs(X) \dot{\sqsubseteq} \rho_\ccs(X)$ since $\rho_\rccs(X)$ contains also the traces with backward actions. In fact, $\rho_\rccs(X) = \rho_\ccs(X) \cup B(\rho_\ccs(X))$. 
\end{itemize}

\subsubsection*{The idea}
Given $\rho_\ccs, \rho_\rccs \in \uco(\wp(\Sigma^\ast))$ such that $\rho_\rccs \sqsubseteq \rho_\ccs$, we want to find a function $f:\wp(\Sigma^\ast) \ra \wp(\Sigma^\ast)$ such that:
\begin{enumerate}
\item the abstract domain $\rho_\ccs(\wp(\Sigma^\ast))$ is not complete for $f$ while the abstract domain $\rho_\rccs(\wp(\Sigma^\ast))$ is complete for $f$, namely one of the following  holds:
\begin{itemize}
\item $\rho_\ccs \circ f \sqsubseteq \rho_\ccs \circ f \circ \rho_\ccs$, meaning that $\rho_\ccs$ is not $\cB$-complete for $f$, while $\rho_\rccs \circ f = \rho_\rccs \circ f \circ \rho_\rccs$ meaning that $\rho_\rccs$ is $\cB$-complete for $f$;
\item $f \circ \rho_\ccs \sqsubseteq \rho_\ccs \circ f \circ \rho_\ccs$, meaning that $\rho_\ccs$ is not $\cF$-complete for $f$, while $f \circ \rho_\rccs = \rho_\rccs \circ f \circ \rho_\rccs$, meaning that $\rho_\rccs$ is $\cF$-complete for $f$.
\end{itemize}
\item $\rho_\rccs$ is the completeness refinement of $\rho_\ccs$ with respect to function $f$, namely one of the followings hold:
\begin{itemize}
\item $\rho_\rccs = \mathcal{R}^\cF_f(\rho_\ccs)$;
\item $\rho_\rccs = \mathcal{R}^\cB_f(\rho_\ccs)$.
\end{itemize}
\end{enumerate}

\subsubsection*{try-1}
Let us consider function $\back: \wp(\Sigma^\ast) \ra \wp(\Sigma^\ast)$ defined as follows:
\begin{itemize}
\item $\back(X) = \sset{\back(\sigma)}{\sigma \in X}$;
\item $\back(\sigma) = \{\sigma l_\bullet ~|~ \sigma = \eta l \nu \nu_\bullet, \eta \in \Sigma^\ast, l \in \Sigma_\circ, \nu \in \Sigma^\ast_\circ, \nu_\bullet \in \Sigma^\ast_\bullet, \nu_\bullet = b(\nu)\}$, where $b(\alpha^1 \dots \alpha^n) = \alpha^n_\bullet \dots \alpha^1_\bullet$;
\item if $\sigma = \nu b(\nu)$ then $\back(\sigma)$ there are no more action that we can revert.
\end{itemize}
we can observe that $\rho_\ccs$ is not $\cF$-complete for $\back$. In fact, we have that $\back(\rho_\ccs(\sigma)) = \sset{\sigma' l l_\bullet}{\sigma' l \in \rho_\ccs(\sigma)}$ while $\rho_\ccs(\back(\rho_\ccs(\sigma))) = \top$, thus $\back \circ \rho_\ccs \sqsubseteq \rho_\ccs \circ \back \circ \rho_\ccs$. Let us compute the $\cF$-completeness refinement of domain $\rho_\ccs$ with respect to function $\back$:
$$
\mathcal{R}^\cF_\back(\rho_\ccs) = \gfp (\lambda X. \rho_\ccs \sqcap \mathcal{M}(\back(X)))
$$
Let us compute the $\gfp$:

$D_0 = \lambda X. \emptyset$\\

\begin{tabular}{ll}
$D_1 =$  & $\rho_\ccs \sqcap \mathcal{M}(\back(D_0))$\\
& $\rho_\ccs \sqcap \lambda X. \top$\\
& $\lambda X. \rho_\ccs(X) \cup \emptyset = \rho_\ccs$\\
\end{tabular}\\

\begin{tabular}{ll}
$D_2  =$ & $\rho_\ccs \sqcap \mathcal{M}(\back(D_1))$\\
& $\rho_\ccs \sqcap \mathcal{M}(\back(\rho_\ccs))$\\
& $\lambda X. \rho_\ccs(X) \cup \back(\rho_\ccs(X))$\\
& $\{ab,abc,abb_\bullet,abcc_\bullet\}$\\
\end{tabular}\\

\begin{tabular}{ll}
$D_3  =$ & $\rho_\ccs \sqcap \mathcal{M}(\back(D_2))$\\
& $\rho_\ccs \sqcap  \lambda X. \back(\rho_\ccs(X)) \cup \back(\back(\rho_\ccs(X)))$\\
& $\lambda X. \rho_\ccs(X) \cup \back(\rho_\ccs(X)) \cup \back(\back(\rho_\ccs(X)))$\\
& $\{ab,abc,abb_\bullet,abcc_\bullet, abb_\bullet a _\bullet,  abcc_\bullet b _\bullet\}$\\
\end{tabular}

\begin{tabular}{ll}
$D_4  =$ & $\rho_\ccs \sqcap \mathcal{M}(\back(D_3))$\\
& $\rho_\ccs \sqcap \lambda X. \back(\rho_\ccs(X)) \cup \back(\back(\rho_\ccs(X))) \cup \back(\back(\back(\rho_\ccs(X))))$\\
& $\lambda X. \rho_\ccs(X) \cup \back(\rho_\ccs(X)) \cup \back(\back(\rho_\ccs(X))) \cup \back(\back(\back(\rho_\ccs(X))))$\\ 
& $\{ab,abc,abb_\bullet,abcc_\bullet, abb_\bullet a _\bullet,  abcc_\bullet b _\bullet, abcc_\bullet b_\bullet a_\bullet\}$\\
\end{tabular}\\

Thus, at the fix point the completeness refinement identifies the domain given by those sets of traces that first go forward and then backward. Namely, we have that 
$$
\mathcal{R}^\cF_\back(\rho_\ccs) = \sset{X \in \wp(\Sigma^\ast)}{X = X_\circ \cup \back^\ast(X)}
$$
where $\back^\ast(X) = \{\back^\ast(\sigma) ~|~ \sigma \in X\}$ and $\back^\ast(\sigma) = \{\back^n(\sigma) ~|~ 1 \leq n \leq |\sigma|\}$.

This does not correspond to the domain $\brccs$.



\subsubsection*{try-2}
Let us consider function $\succ: \wp(\Sigma^\ast) \ra \wp(\Sigma^\ast)$ defined as follows:
\begin{itemize}
\item $\succ(X) = \sset{\succ(\sigma)}{\sigma \in X}$;
\item $\succ(\sigma) = \back(\sigma) \cup \next(\sigma)$;
\item $\next(\sigma) = \{\sigma l ~|~ l \in \Sigma_\circ\}$ {\bf deve essere il next rispetto alla relazione di transizione di CCS +++ sistema}
\end{itemize}
we can observe that $\rho_\ccs$ is not $\cF$-complete for $\succ$. In fact, we have that 
$$
\succ(\rho_\ccs(\sigma)) = \sset{\back(\sigma')}{\sigma' \rho_\ccs(\sigma)} \cup \sset{\next(\sigma')}{\sigma' \in \rho_\ccs(\sigma)}
$$
while $\rho_\ccs(\succ(\rho_\ccs(\sigma))) = \top$, thus $\succ \circ \rho_\ccs \sqsubseteq \rho_\ccs \circ \succ \circ \rho_\ccs$. Let us compute the $\cF$-completeness refinement of domain $\rho_\ccs$ with respect to function $\succ$:
$$
\mathcal{R}^\cF_\succ(\rho_\ccs) = \gfp (\lambda X. \rho_\ccs \sqcap \mathcal{M}(\succ(X)))
$$
Let us compute the $\gfp$:

$D_0 = \lambda X. \emptyset$\\

\begin{tabular}{ll}
$D_1 =$  & $\rho_\ccs \sqcap \mathcal{M}(\succ(D_0))$\\
& $\rho_\ccs \sqcap \lambda X. \top$\\
& $\lambda X. \rho_\ccs(X) \cup \emptyset = \rho_\ccs$\\
\end{tabular}\\

\begin{tabular}{ll}
$D_2  =$ & $\rho_\ccs \sqcap \mathcal{M}(\succ(D_1))$\\
& $\rho_\ccs \sqcap \mathcal{M}(\succ(\rho_\ccs))$\\
& $\lambda X. \rho_\ccs(X) \cup \back(\rho_\ccs(X)) \cup \next(\rho_\ccs(X))$\\
& $\{ab,abc,abb_\bullet,abcc_\bullet,abd, aba, abca, abcb, \dots\}$\\
\end{tabular}\\

\begin{tabular}{ll}
$D_3  =$ & $\rho_\ccs \sqcap \mathcal{M}(\succ(D_2))$\\
& $\lambda X. \rho_\ccs(X) \cup \back(\rho_\ccs(X)) \cup \next(\rho_\ccs(X)) \cup \back(\back(\rho_\ccs(X)))$\\
& $ \cup \next(\back(\rho_\ccs(X))) \cup \back(\next(\rho_\ccs(X))) \cup \next(\next(\rho_\ccs(X))$\\
& $\{ab,abc,abb_\bullet,abcc_\bullet,abd, aba, abca, abcb, \dots, abb_\bullet a_\bullet, abcc_\bullet b_\bullet, abb_\bullet b, abb_\bullet a \dots,$\\
& $ abcc_\bullet a, \dots,  abdd_\bullet,abcaa_\bullet, abdc, abaa,abcaa,\dots \}$\\
\end{tabular}\\

\begin{theorem}
At the fix point we have that $\mathcal{R}^\cF_\succ(\rho_\ccs) = \rho_\rccs$.
\end{theorem}
{\sc proof:} {\bf to be done}


\bibliographystyle{abbrv}

\bibliography{biblio}%style{abbrv}
\bibliographystyle{plain}

%\begin{thebibliography}{}

%\end{thebibliography}

%\newpage

\end{document}

